Section: Software

Vercors platform

Participants : E. Madelaine, R. Halalai, L. Henrio, A. Savu, M. Alexe.

The Vercors tools (http://www-sop.inria.fr/oasis/Vercors ) include front-ends for specifying the architecture and behaviour of components in the form of UML diagrams. We translate these high-level specifications, into behavioural models in various formats, and we also transform these models using abstractions. In a final step, abstract models are translated into the input format for various verification toolsets. Currently we mainly use the various analysis modules of the CADP toolset.

• Our main effort this year was based on the development of a quite large case-study, two orders of magnitude larger than our previous experiments. This study was the opportunity to develop new methods for encoding our models using a new combination of CADP formalisms, combining compositional approaches, abstraction techniques, and distributed model-checking [22] . The implementation of these methods in the Vercors tools has started.

  We have also been conducting experiments towards the next generation of specification formalism editors for VerCors, using the Papyrus UML-based environment.